(set-logic QF_UF)
(declare-fun uf3 (Bool Bool Bool) Bool)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(push 1)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(push 1)
(declare-fun v8 () Bool)
(assert v0)
(push 1)
(declare-sort S0 0)
(declare-fun v9 () Bool)
(declare-fun v10 () Bool)
(declare-fun v11 () Bool)
(assert v6)
(assert (distinct v10 (not v3)))
(assert (uf3 v8 (not v3) (distinct v10 (not v3))))
(declare-fun S0-0 () S0)
(push 1)
(push 1)
(assert (not v7))
(check-sat)
(declare-sort S1 0)
(declare-fun v12 () Bool)
(assert (=> v1 v7))
(assert (uf3 v11 v2 v10))
(assert (not (not v3)))
(check-sat)
